(DEFPROP ATTEMPT 
 (LAMBDA(L S C)
  (PROG (NEWNAME SUPPORT
 		 UNITPF
 		 LCL
 		 LVL
 		 CNT
 		 XYZ2
 		 LSTCLS
 		 LLST
 		 Z1
 		 MERGE
 		 ORDER
 		 DEBUG
 		 DEPTH
 		 LENGTH
 		 ANCESTRY
 		 STRATEGY
 		 STRAT
 		 PMODEL
 		 NMODEL
 		 PFLG
 		 EQUAL
 		 PDEPTH
 		 DLIST
 		 XYZ
 		 XYZ1
 		 COND
 		 Z
 		 UNAXP
 		 UNAXN
 		 SAT
 		 EXTERM
 		 E1
 		 E2
 		 B2
 		 XX
 		 CLAUSES
 		 SUBCLAUSES
 		 COUNT
 		 SLENGTH
 		 ORDLST
 		 OCLIST)
	(SETQ NEWNAME (LIST (LIST NIL)))
	(SETORD (CAR L) (CDR L))
	(SETQ Z (MINIMIZE (CAR L)))
	(UPDATESTATE (COND ((NULL S) (SETQ STRAT (SETQUERY Z))) (T (SETQ STRAT S))))
	(SETQ COND C)
	(SETQ XYZ2 Z)
	(SETQ LVL 1)
	(SETQ COUNT 0)
	(SETQ Z (UNITPN XYZ2))
	(SETQ UNAXP (CAR Z))
	(SETQ UNAXN (CDR Z))
	(SETQ CLAUSES XYZ2)
	(COND ((NOT PFLG) (SETQ UNAXP (CONS (SET2 (LIST (LIST 1 NIL) (LIST EQUAL 0 0))) UNAXP))
			  (SETQ SUBCLAUSES (CONS (CAR UNAXP) CLAUSES)))
	      (T (SETQ SUBCLAUSES CLAUSES)))
	(SETQ LCL (LAST CLAUSES))
	(SETQ LSTCLS LCL)
	(SETQ CNT (ADD1 (LENGTH XYZ2)))
	(SETQ AXNO 201)
	(SETQ Z1 (ERRSET (TRYPRF (COND (ANCESTRY (SETQ LLST (INITIAL XYZ2 -1000 1000))) (T XYZ2)))))
	(COND ((OR (EQ Z1 (QUOTE NOPROOF)) (NULL Z1)) (RETURN (CONS (QUOTE NOPROOF) (CONS CLAUSES STRAT))))
	      ((EQ (CAR Z1) (QUOTE QED)) (SETQ Z
					       (EVAL
						(LIST (QUOTE OUTC)
						      (LIST (QUOTE OUTPUT) (QUOTE PRF) (QUOTE DSK:) FILENAM)
 						      NIL)))
					 (QUERY)
					 (PROOF LHP RHP)
					 (OUTC Z T)
					 (RETURN Z1))
	      (T (RETURN Z1))))) 
EXPR)